$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $i$, $u$:$T$. ($i$ = $u$) $\Rightarrow$ ($P$($u$)) $\Rightarrow$ ($i$ = $u$ $\in$ \{$j$:$T$$\mid$ \{$j$:$T$$\mid$ $P$($j$)\} \} )